Abstractions for hybrid systems
Identifieur interne : 004D17 ( Main/Exploration ); précédent : 004D16; suivant : 004D18Abstractions for hybrid systems
Auteurs : Ashish Tiwari [États-Unis]Source :
- Formal Methods in System Design [ 0925-9856 ] ; 2008-02-01.
English descriptors
Abstract
Abstract: We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.
Url:
DOI: 10.1007/s10703-007-0044-3
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001E18
- to stream Istex, to step Curation: 001D95
- to stream Istex, to step Checkpoint: 001102
- to stream Main, to step Merge: 004E51
- to stream Main, to step Curation: 004D17
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Abstractions for hybrid systems</title><author><name sortKey="Tiwari, Ashish" sort="Tiwari, Ashish" uniqKey="Tiwari A" first="Ashish" last="Tiwari">Ashish Tiwari</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:8213F313ABB512ED9F185E98E24159FB0521BEA4</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/s10703-007-0044-3</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-3M5V64DC-S/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001E18</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001E18</idno><idno type="wicri:Area/Istex/Curation">001D95</idno><idno type="wicri:Area/Istex/Checkpoint">001102</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001102</idno><idno type="wicri:doubleKey">0925-9856:2007:Tiwari A:abstractions:for:hybrid</idno><idno type="wicri:Area/Main/Merge">004E51</idno><idno type="wicri:Area/Main/Curation">004D17</idno><idno type="wicri:Area/Main/Exploration">004D17</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Abstractions for hybrid systems</title><author><name sortKey="Tiwari, Ashish" sort="Tiwari, Ashish" uniqKey="Tiwari A" first="Ashish" last="Tiwari">Ashish Tiwari</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>SRI International, 333 Ravenswood Ave., Menlo Park, CA</wicri:regionArea><placeName><region type="state">Californie</region></placeName></affiliation><affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Formal Methods in System Design</title><title level="j" type="sub">An International Journal</title><title level="j" type="abbrev">Form Methods Syst Des</title><idno type="ISSN">0925-9856</idno><idno type="eISSN">1572-8102</idno><imprint><publisher>Springer US; http://www.springer-ny.com</publisher><pubPlace>Boston</pubPlace><date type="published" when="2008-02-01">2008-02-01</date><biblScope unit="volume">32</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="57">57</biblScope><biblScope unit="page" to="83">83</biblScope></imprint><idno type="ISSN">0925-9856</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0925-9856</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Hybrid systems</term><term>Predicate abstraction</term><term>Qualitative simulation</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.</div></front></TEI><affiliations><list><country><li>États-Unis</li></country><region><li>Californie</li></region></list><tree><country name="États-Unis"><region name="Californie"><name sortKey="Tiwari, Ashish" sort="Tiwari, Ashish" uniqKey="Tiwari A" first="Ashish" last="Tiwari">Ashish Tiwari</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004D17 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004D17 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:8213F313ABB512ED9F185E98E24159FB0521BEA4
|texte= Abstractions for hybrid systems
}}
| This area was generated with Dilib version V0.6.33. |  |